Інформатика
Мотивація
Важливим етапом в розвитку викладача є не тільки програма для вищої школи четвертого рівня акредитації, але і для середньої школи, а значить кожного учня в кожному селі. Для цих потреб за основу я хочу взяти програму "Інформатика" Манфреда Броя.
Власне, оскільки школа починається з 5 років приблизно, то цей курс у вигляді монографії повинен відповідати вимогам ELI5, шоб кожен вчитель міг відтворити цей курс.
Структура курсу Манфреда Броя
Шо гарного я можу сказати про цю програму: 1) це фулстек програма, яка покриває розробку мовних засобів, дискретну математику і паралельне програмування 2) програма викладається штучно створеною педагогічною мовою для цього типу паскаля 3) логіку починає з Арістотеля.
Чотири теми мого курсу Інформатика наслідують розділ на чотири книги Манфреда Броя і мають наступну структуру:
1) Основи: інформація, алгоритми і структури, мови, їх класи, типи, рекурсія:
— Інформація, інформаційна система та її властивості.
— Позиційні системи числення, кодування інформації.
— Алгоритми, системи переписування термів, ג-числення, рекурсивні функції.
— Типи і структури даних, Бом дерева, структурна рекурсія.
— Логіка висловлювань, логіка предикатів, вищі логіки.
— Мови програмування, граматики, БНФ, лексичний аналіз.
2) Дискретна математика, схемотехніка, асемблери;
— Булева алгебра та редукція термів. ДНФ, КНФ.
— Регістри, Лічильники, Логіка, Арифметика.
— Архітектура компʼютера. SMP, AMP.
— Узгоджена паралельна обробка черг.
3) Операційні системи, компілятори, рантайми;
— Числення процесів. Моделі процесів. Мережі Петрі, FSM автомати, BPMN.
— Операційні системи і рантайми. Реактори, Процеси, Канали, Курсори.
— Мови. Лексика, Синтаксис. LL, LR, LALR. Інтерпретатори, Компілятори.
4) Формальні мови, обчислювальність, складність, ефективність.
— Формальні мови. Основи математики.
— Обчислювальність. Коректність. Складність. Ефективність.
— Семантика мов програмування. Формальні моделі.
— Мова опису математики.
Інформація, алгоритми і структури даних, мови, типи, рекурсія.
Дискретна математика і схемотехніка.
Операційні системи, рантайми, інтерпретатори і компілятори.
Формальні мови, обчислювальність, коректність, слкадність, ефективність.
Компілятор мови ML Робіна Мілнера
Оскільки четверта тема є добре пропрацьованою в курсі "Формальна математика", а операційна система з третьої теми теж частина цієї монографії, то найскладніша і націкавіша теми, з якої хочеться почати --- це "Компілятор", який є частиною третьої теми курсу.
Я провів в дослідженні компіляторів, мов програмування і операційних систем 20 років, починаючи від embedded систем TRON, QNX, BeOS до дизасемблювання NT в Soft-ICE і хочу сказати шо ті школи які взяли у якості основи серію мов Standard ML мають неабияку перевагу. Я провів свою юність з мовами серії ML лише поверхово (написали веб-сокет сервер, портували на SML N2O та NITRO), але вже тоді схопив найголовніше: мова ML це єдина промислова мова рівня System F з доведеною семантикою і теоремами про коректність (soundness) написаними в Twelf, головна заслуга тут Роберта Харпера. Мова програмування Standard ML була придумана Робіном Мілнером за яку він дістав премію Тюрінга, один з небагатьох хто заслужено.
Тому замість Pascal/Ada-подібної мови Манфреда Броя, на якій наводяться приклади алгоритмів з його курсу "Інформатика" в нашому курсі ми пропонуємо використовувати ML мову MinCaml розроблену Ейдзіро Суміі в Університеті Токіо.